perm filename MTC.PRO[1,JMC] blob
sn#188572 filedate 1973-04-01 generic text, type T, neo UTF8
%,2
Proposal for Research
in
Mathematical Theory of Computation
John McCarthy, Professor of Computer Science
Principal Investigator
Submitted to the
National Aeronautics and Space Administration
July 1970
Computer Science Department
School of Humanities and Sciences
Stanford University
%B,2
Abstract
$33,500 is requested for research in Mathematical Theory of
Computation for the first year of a three year program.
Table of Contents
page
Introduction.................................................... 2
The Present State of Mathematical Theory of Computation......... 5
The Proposed Research........................................... 16
Key Personnel................................................... 17
Budget.......................................................... 21
Cognizant Personnel............................................. 22
References...................................................... 23
Introduction
This is a request for support to carry out research in mathematical
theory of computation over a period of three years. The research
will be oriented towards the applied goal of replacing much debugging
by computer-checking formal proofs that computer programs meet their
specifications. The work will be done in the Artificial Intelligence
Project of the Computer Science Department of Stanford University
which has already done considerable work in this area, but we will
need the support requested in this proposal to bring the technique to
the point of practical application.
The reasons for expecting useful results from research oriented at
using proof checkers to assist and replace debugging are briefly as
follows.
1. Since a computer program is a mathematical object, its
specifications can often be stated in purely mathematical terms and
the fact that it meets them is often a purely mathematical fact.
2. The specifications that the program must meet can usually be
stated much more briefly than the program itself and are much more
clearly understandable than the program. Of course, this is
dependent on having a good notation for expressing these
specifications. Moreover, many partial specifications such as that
the program shall not go into a loop or use storage not assigned to
it are particularly easy to state.
3. The informal arguments in the mind of a programmer as he
writes are never deep and therefore should be readily expressible
formally given a suitable language for doing so.
4. For the same reason, a computer program that checks these
proofs of correctness should offer no difficulties of principle.
5. The confidence of a user in a program that has been proved to
be correct will be much greater than that in a program that has
merely been tested on a number of cases. We look forward to the time
when no-one will pay money for a program that is not proved to meet
its specifications.
The road to this goal has quite a few practical difficulties that the
proposed research is aimed at overcoming. Among these are:
1. A convenient formalism for writing the specifications does
not yet exist.
2. The formal languages of mathematical logic are really
designed for proving metatheorems rather than for convenient use. We
shall have to devise a language allowing many modes of expression
that are presently only used informally.
3. The practical use of a proof checking system by programmers
will require an an interactive system in which each step of the
reasoning is checked as soon as possible. It may even be best that
the programmer be given the ability to check assertions about
statements or subprograms as soon as he writes the subprogram in
question. This may be especially useful for the standard
specifications of non-looping and non-interference with other
storage.
4. Finally and perhaps most important, there is yet much work to
be done to get the proper axioms and rules of inference and to
describe the semantics of the formal system we need.
In the remaining sections of this proposal we shall give the history
of mathematical theory of computation, the present state of that
theory, the specific research goals of this project, the personnel
active in the work, the facilities of the Stanford Artificial
Intelligence Laboratory, and finally a budget.
The Present State of Mathematical Theory of Computation
Verifying that a computer program meets its specifications may
involve verifying that it interacts with the world outside the
computer correctly, and so may involve knowledge of the properties of
the world as well as of the program itself. However, many of the
desired properties of a program are purely mathematical consequences
of its structure. Indeed, for most programs all the desired
properties such as termination, affecting only its own storage,
having a prescribed relation between its inputs and outputs, are
mathematical. Therefore, instead of debugging a program, i.e.
testing its operation on a limited number of cases, it should, in
principle, be possible to prove that the program meets its
specifications. Mathematical theory of computation is concerned with
formalizing the properties of computer programs that constitute their
correctness, developing techniques for expressing and proving
correctness, and also with computer programs that can verify proofs
of correctness, and even with programs that might generate proofs of
correctness.
We cannot expect to be able to find a general technique for
generating proofs of correctness of programs. The problems are in
general undecidable and can involve the solution of arbitrary
problems of the field of knowledge the program is concerned with. An
extreme example of this would be given by a program for adding four
integers that did it in the usual way except when the four numbers
came out to be a counter-example to Fermat's last theorem, in which
case it returns 0. Whether the program adds correctly depends on
whether Fermat's last theorem is true. Incidentally, we also see
that there is no way of debugging the program since it will work
correctly on all cases except for counter-examples to Fermat's last
theorem. Although this example is artificial, the domain of
interesting programs has the property that there is no general method
of proving programs correct and, moreover, no general way of
constructing test cases for debugging.
On the other hand, expressing the correctness of programs formally
and formally verifying proofs of their correctness seems intuitively
to be a feasible goal. When a person writes a program, he has an
intuitive idea of what the program is supposed to do, and as he
writes it , he has intuitive reasons for expecting the steps of the
program to do the right thing. The errors made are generally
oversights and when an oversight is pointed out, the programmer
usually understands his mistake even though it may not be apparent to
him how to change the program so that it will meet the
specifications. Therefore, our problem is merely one of expressing
in a formal mechanically checkable way reasonings that, in themselves
are not difficult.
There is a close formal relation between mathematical theory of
computation as described above and the older theory of computable
functions. In fact, they deal with the same objects since computer
programs are entirely equivalent to Turing machines or any of the
other formalisms they use to describe algorithms. Unfortunately for
us, their objectives are so different from ours that only the most
elementary of their results are relevant to proving that particular
programs meet their specifications. Namely, the theory of
computability is concerned with what classes of problems can be
solved by computable functions and various subclasses and
generalizations thereof. It is never concerned with the properties
of specific algorithms.
Another related field is automata theory. Sometimes its results are
relevant for theory of computation, but it too is not often concerned
with the properties of specific programs.
A final relevant theory is formal syntax. This has been helpful in
defining the set of admissible strings of programming languages, but
the definitions have usually not taken a form that permits an equally
formal definition of their semantics. Some recent work of Knuth
(1968) deals with the problem of assigning semantics to context-free
languages by definitions that parallel the productions that define
the syntax. It turns out in some of Knuth's examples, that even when
the syntax is context-free, the semantics of an expression depends on
the context.
The goal of using mathematical theory of computation to replace
debugging was first stated in (McCarthy 1963a), but some results
significant for realizing this goal were obtained earlier. In (Yanov
1960), programs were represented by block schemata which are
essentially the same as flow charts. A notion of equivalence of
block schemata was defined and a decision procedure for this
equivalence was given. The Soviet school of "theory of programming",
as they call it, has mainly concentrated on developing and
elaborating Yanov's notion. Equivalence of schemata is stronger
than equivalence of programs in that two equivalent programs (in the
sense that for the same inputs they give the same outputs) may have
inequivalent schemata. In fact, the transformations that preserve
Yanov equivalence are so limited that no one has tried to apply them
to actual programs.
Yanov schemata can be regarded as Algol programs using only
assignment statements of the form x := f(x) and go to's of the form
if p(x) then go to a;
with the further restriction that there is only one variable x in the
whole program. Equivalence of schemata means input-output
equivalence for all domains of the variable and all interpretations
of the function and predicate letters. Yanov showed that this
equivalence is decidable even with certain additional conditions
about the effect of executing the assignment statements on the values
of the predicates. See (Rutledge 1964) for details.
The decidability of Yanov schemata goes away, however, if we allow
two different variables or impose algebraic relations among the
functions. This is shown in (Luckham and Park 1964).
Semi-definitive results in this direction were obtained by Manna
(1968), who allows first order axioms to relate the functions and
predicates and shows that termination is equivalent to the truth of a
formula of predicate calculus. He also can treat relations between
input and output and equivalence under the conditions that both
programs terminate for given inputs.
It turns out, however, that almost all interesting results concerning
actual programs require mathematical induction for their proof. In
first order formulations this means that axiom schemata and not just
finite sets of axioms are required. In fact, the termination of a
program is equivalent to an axiom schema; the usual induction schema
of first order arithmetic is equivalent to the termination of a
program that starts with a given integer and counts down until it
reaches zero.
The first formalized use of induction for proving equivalence and
other properties of programs is in (McCarthy 1963a) wherein a method
called recursion induction was given for proving equivalence and
relations between the arguments and values of functions defined
recursively using conditional expressions. (This paper is probably
also the first to describe the potential use of mathematical theory
of computation to replace debugging.) Examples of proofs were given
for the elementary functions of integers and also for LISP functions
of symbolic expressions. The method was further developed and
extended to Algol-like programs in (McCarthy 1963b).
Floyd (1967) gave another method of proving properties of Algol-like
programs. The two methods are equally powerful but apparently not
equivalent; Floyd's method is more intuitive for Algol-like programs.
Neither method treats termination and require that the termination of
programs be established by other (at that time unformalized) methods.
Manna (1969a and b) recast Floyd's formalism radically so as to be
able to treat termination and McCarthy discovered how to recast his
own formalization so as also to treat termination. Manna and Pnueli
(1969c) showed how to unify the recursive function and Algolic
program results. Each formalism has its advantages for different
classes of problems. (The recursive function formalism is more easily
manipulated mathematically when the problem fits that form, but this
is not always the case.)
A second main line of development of mathematical theory of
computation is the semantic definition of programming languages. This
makes possible proofs of the correctness of translators. This
started with (McCarthy 1963b) which introduces the notion of abstract
syntax, a syntactic tool that permits the convenient definition of
semantics and the description of translators. This paper also shows
how to define semantics by a recursive interpreter using a state
vector and also gives a definition of the correctness of a
translator. This is applied to defining the semantics of a subset of
Algol in (McCarthy 1966) and to proving the correctness of a
translator for arithmetic expressions in (McCarthy and Painter 1967).
Painter (1967) extended the method to proving the correctness of
translators for simple Algolic programs. These proofs involved
rather complicated formalism which discouraged attempts to apply the
method to more complicated languages. A new approach by Morris (1970
we hope) seems to avoid these complications.
The ideas of abstract syntax and state vectors were used by the IBM
Vienna group ( Lucas et. al. 1968) to define the semantics of PL/I,
but they got into severe complications in the description, partly due
to the many anomalies in PL/I. The mathematical properties of their
notation have not as yet been formalized and it is not clear that
they will be able to treat correctness of translators.
Other purely descriptive formalisms are those of Landin (languages
are described by giving rules for translation into lambda calculus),
van Wijngarten (languages are described by giving their data as
strings and giving Markov-like algorithms for the elaboration of the
computation), the formalism of de Bakker (1968), and the lambda
calculus formalism of (Ledgard 1969). In our opinion, the usefulness
of a descriptive formalism is, in the long run, determined by its
usability for the description of translation procedures and proofs of
their correctness. In this connection, the results of Donovan and
Ledgard (1967) are interesting in that they apply Donovan's canonic
systems to the complete syntactic description of programming
languages, including the restrictions (such as that an identifier
used in a go to statement must appear exactly once as a label) that
cannot be described in Chomsky type languages. Donovan's methods
also allow the relation between a source program and certain
translations of it to be defined. We hope to be able to use some of
his ideas in connection with abstract syntax.
Another relevant line of work is the development of partial predicate
calculus in mathematical logic. The formalisms described in (Wang
1961), (McCarthy 1963c), and (Hayes 1969) provide a formalism in
which proofs of correctness of programs can be made (Manna and
McCarthy, 1970) because computable functions can be substituted in
their valid formulas without first determining that they are total,
i.e. that the algorithms terminate.
The development of resolution methods of theorem proving starting
with (Robinson 1965) provide a basis for writing proof checkers that
can also do part of the work of constructing the proof. Proof
checkers in general are discussed in (McCarthy 1964) and one for
resolution proofs is described in (McCarthy 1965).
In the last year, a number of new approaches have appeared. Burstall
(1970) applies first order logic to describing both the syntax and
the semantics of an extensive Algol subset. By using the axiom
schema of mathematical induction, he can prove the correctness and
termination of simple programs.
Scott (1970) has defined a partial function theory analogous to set
theory that contains partial functions of higher types. The
undefined element of each type and a partial ordering according to
relative definedness are introduced. Recursion is introduced by a
combinator that gives the least fixed point of a partial function.
The axioms include a direct generalization of recursion induction.
Park (1970) has used the Knaster-Tarski fixpoint theorem for complete
lattices to give a fixpoint theorem for predicate calculus formulas.
By appropriate choice of formulas, the theorem gives
i) the results of Manna and Prueli (1969c) for recursively
defined functions
ii) a statement of recursion induction, and
iii) certain interesting properties of the interpretations
satisfying the formula (e.g. the appropriate induction
principle for such interpretations).
Recent work (1970) in the AI Project
Ashcroft and Manna (1970) have extended the methods of Floyd and
Manna to parallel programs. Although the programs considered are
syntactically simple, they do exhibit interaction between
asynchronous parallel processes. The formalization can be extended
to more complicated programs. The method is based on a
transformation of parallel programs into non-deterministic programs,
the properties of which have been formalized in Manna (1970a). The
nondeterministic programs are in general much larger than the
parallel programs they correspond to. A simplification method is
therefore presented which, for a given parallel program, allows the
construction of a simple equivalent parallel program, whose
corresponding non-deterministic program is of reasonable size.
Manna (1970b) demonstrates conclusively that all properties regularly
observed in programs (deterministic or non-deterministic) can be
formulated in terms of a formalization of 'partial correctness'.
Ashcroft (1970) 'explains' this by formulating the notion of an
intuitively 'adequate' definition (in predicate calculus) of the
semantics of a language or a program. He shows the relationship
between a formalization or partial correctness of a program and an
'adequate' logical definition of its semantics.
Manna and Ness (1970) have formalized techniques for proving the
termination of algorithms using well-ordered sets. They give
effective sufficient conditions for termination as well as
non-effective necessary and sufficient conditions.
Manna and McCarthy (1970) formalize properties of Lisp-like programs
using partial function logic, where the partial functions occuring in
the formulas are exactly those computed by the programs. They
distinguish between two types of computation rules--sequential and
parallel.
Among work in progress, Igarashi is developing further axiomatic
methods for the semantics of Algol-like languages, mainly based on
his earlier studies, but allowing the methods of Floyd to be carried
out within the formalism. A metatheorem is included which can be
interpreted as a proof of correctness of a conceptual compiler for
the programs treated by the formalism.
In summary, mathematical theory of computation has become a lively
discipline, and much of the work is oriented in directions that will
eventually enable us to replace most debugging.
The Proposed Research
In view of the above described state of mathematical theory of
computation, we propose to carry out the following research:
1. To develop further the theory of equivalence, termination and
correctness of computer programs.
2. To develop further the theory of semantic definition of
programming languages, the formal description of translation
algorithms, and the correctness of compilers.
3. To try to develop a theory of parallel processes adequate to
prove their correctness and especially their mutual non-interference.
4. To develop a formal system of logic in which proofs of
termination, equivalence, correctness, and non-interference can be
conveniently expressed.
Key Personnel
The key ingredient in a research project is able and knowledgeable
personnel. The Stanford Computer Science Department has a major
concentration of people who have made contributions to the
Mathematical Theory of Computation. Biographies of key individuals
who will participate in this project are given below.
The research staff will be able to draw on the experience of
well-known members of the Computer Science Department, including:
Robert Floyd (Theory of Computation), Donald Knuth (Theory of
Algorithms), Jerome Feldman (Programming Languages), and David
Luckham (Automatic Theorem Proving). Other partcipants will include
Shigeru Igarashi and Amir Pnueli, who have recently developed some
important results in Mathematical Theory of Computation. Several
system programmers will be involved who have had experience in
developing the time-sharing computer facility of the Artificial
Intellligence Project.
%B,1
NAME: John McCarthy
BORN: September 4, 1927 in Boston, Massachusetts
EDUCATION:
B.S. (Mathematics), California Institute of Technology, 1948
Ph.D. (Mathematics), Princeton University, 1951
HONORS AND SOCIETIES:
American Mathematical Society
Association for Computing Machinery
Institute for Electrical and Electronic Engineers
Sigma Xi
Sloan Fellow in Physical Science, 1957-59
ACM National Lecturer, 1961
PROFESSIONAL EXPERIENCE:
Proctor Fellow, Princeton University, 1950-51
Higgins Research Instructor in Mathematics, Princeton
University, 1951-53
Acting Assistant Professor of Mathematics, Stanford
University, 1953-55
Assistant Professor of Mathematics, Dartmouth College,
1955-58
Assistent Professor of Communication Science, M.I.T., 1958-61
Associate Professor of Communication Science, M.I.T., 1961-62
Professor of Computer Science, Stanford University,
1962-present.
PROFESSIONAL RESPONSIBILITIES AND SCIENTIFIC INTERESTS:
With Marvin Minsky, organized and directed the Artificial
Intelligence Project at M.I.T.
Developed the LISP programming system for computing with
symbolic expressions.
Participated in the development of the ALGOL 58 and ALGOL 60
languages.
Organized and directs the Stanford Artificial Intelligence
Project.
Present scientific work is in the fields of Artificial
Intelligence, Computation with Symbolic Expressions,
Mathematical Theory of Computation, and Time-Sharing
Computer Systems.
PUBLICATIONS:
References 17 and 19-25 plus the following;
1. "Projection Operators and Partial Differential
Equations", Ph.D. Thesis, Princeton University, 1951.
2. "A Method for the Calculation of Limit Cycles by
Successive Approximation" in Contributions to the Theory
of Nonlinear Oscillations II, Annals of Mathematics Study
No. 29, Princeton University, 1952, pp. 75-79.
3. "An Everywhere Continuous Nowhere Differentiable
Function", American Mathematical Monthly, December 1953,
p.709.
4. "A Nuclear Reactor for Rockets", Jet Propulsion, January
1954.
5. "The Inversion of Functions Defined by Turing Machines"
in Automata Studies, Annals of Mathematics Study No. 34,
Princeton, 1956, pp. 177-181.
6. Co-editor with Dr. Claude E. Shannon of Automata Studies,
Annals of Mathematical Study No. 34, Princeton, 1956.
7. "Recursive Functions of Symbolic Expressions and their
Computation by Machine", Comm. ACM, April 1960.
8. "Programs with Common Sense", Proc. Teddington Conf. on
Mechanization of Thought Processes, H. M. Stationary
Office, 1960.
9. (with 12 others) "ALGOL 60", Comm. ACM, May 1960 and Jan.
1963, and Numerische Mathematik, March 1960.
10. "A Basis for Mathematical Theory of Computation", Proc.
Western Joint Computer Conf., May 1961, pp. 225-238.
11. "Time-Sharing Computer Systems" in Management and the
Computer of the Future (Greenberger, ed.), MIT Press,
1962.
12. (with Abrahams, Edward, Hart, and Levin) LISP 1.5
Programmers Manual, MIT Press, 1962.
13. Computer Programs for Checking Mathematical Proofs",
Amer. Math. Soc. Proc. Symposia in Pure Math., Vol. 5,
1962.
14. (with Boilen, Fredkin, and Licklider) "A Time-Sharing
Debugging System for a Small Computer", Proc. AFIPS 1963
Spring Joint Computer Conf., Spartan, Detroit, 1963.
15. (with F. Corbato and M. Daggett) "The Linking Segment
Subprogram Language and Linking Loader Programming
Languages", Comm. ACM, July 1963.
16. "Time-Sharing Computer Systems" in Conversational
Computers (W. Orr, ed.), Wiley, 1966.
17. "Information", Scientific American, Sept. 1966.
18. (with D. Brian, G. Feldman, and J. Allen) "THOR - A
Display Based Time-Sharing System", AFIPS Conf. Proc.,
Vol. 30 (FJCC), Thompson, Washington D. C.,1967.
19. "Computer Control of a Hand and Eye", Proc. Third
All-Union Conference on Automatic Control (Technical
Cybernetics), Nauka, Moscow, 1967 (Russian).
20. "Programs with Common Sense" in Semantic Information
Processing (M. Minsky, ed.), MIT Press, 1968.
21. (with Earnest, Reddy, and Vicens) "A Computer with
Hands, Eyes and Ears" Proc. AFIPS Conf. 1968 (FJCC).
22. (with P. Hayes) "Some Philosophical Problems from the
Standpoint of Artificial Intelligence" in Machine
Intelligence 4 (D. Mitchie, ed.), American Elsevier, New
York, 1969.
NAME: Zohar Manna
BORN: Jan. 17, 1939 in Haifa, Israel
EDUCATION:
B.Sc. (Mathematics), Technion, Haifa, Israel, 1962
M.Sc. (Mathematics), Technion, Haifa, Israel, 1965
Ph.D. (Computer Science), Carnegie-Mellon University, 1968
PROFESSIONAL EXPERIENCE:
First Lieutenant, Programming, Israel Defense Forces, 1962-64
Teaching Assistant in Mathematics, Technion, Haifa, Israel,
1962-64
Research Assistant in Computer Science, Carnegie-Mellon
University, 1965-68
Assistant Professor of Computer Science, Stanford University,
1968-present.
SCIENTIFIC INTERESTS:
Matematical Theory of Computation
Mathematical Logic
Graph Theory and Automata Theory
Formal Systems
Optimization Techniques
PUBLICATIONS:
References 2 and 12-18 plus the following;
1. "Formalization of Properties of Programs", Memo AI-64,
Computer Science Dept., Stanford University, July 1968.
2. (with A. Pnueli) "The Validity of the 91-Function" Memo
AI-68, Computer Science Dept., Stanford University,
August 1968.
3. "Termination of Interpreted Graphs", submitted to JACM.
NAME: Ed Ashcroft
BORN: July 15, 1944 in Ormskirk, England
EDUCATION:
B.A. (Mechanical and Electrical Sciences), Cambridge
University, England, 1966
Ph.D. studies, thesis to be submitted, Centre for Computing
and Automation, Imperial College of Science and
Technology, London.
PROFESSIONAL EXPERIENCE:
Research Associate in Computer Science, Stanford University,
1969-present.
SCIENTIFIC INTERESTS:
Mathematical Theory of Computation
Artificial Intelligence
Cosmology
PUBLICATIONS:
References 1 and 2.
%B,1
Budget for the period 1 October 1970 through 30 September 1971
I. Salaries
McCarthy, J. 3,923
Prof. Of Computer Science
10% time Acad. Yr., 25% summer
Manna, Z. 2,273
Asst. Prof., Computer Science
10% Acad. Yr., 25% Summer
Ashcroft, E. 2,640
Research Associate
20% time
Graduate Student 5,200
50% Acad. yr., 100% Summer
Secretary 1,600
25% time
Administrative support 1,850
10% time
TOTAL SALARIES 17,486
II. STAFF BENEFITS
13.9% of salaries 2,431
III.INDIRECT COSTS
59% of salaries 10,317
IV. TRAVEL
One trip East 450
V. COMMUNICATIONS
Telephone 250
VI. OTHER OPERATING EXPENSES 2,566
TOTAL PROJECT COST 33,500
Cognizant Personnel
For contractual matters:
Office of the Research Administrator
Stanford University
Stanford, California 94305
Telephone: (415) 321-2300, ext. 2883
For technical and scientific matters:
Prof. John McCarthy
Computer Science Department
Stanford University
Stanford, California 94305
Telephone: (415) 321-2300, ext. 4971
For administrative matters, including questions
relating to the budget or property acquisition:
Mr. Lester D. Earnest, Executive Officer
Artificial Intelligence Project
Computer Science Department
Stanford University
Stanford, California 94305
Telephone: (415) 321-2300, ext. 4971
References
1. E.A. Ashcroft, (1970), "Mathematical Logic Applied to the
Semantics of Computer Programs", Ph.D. Thesis, to be submitted
to Imperial College, London.
2. E.A. Ashcroft and Z. Manna, (1970), "Formalization of Properties
Parallel Programs", Stanford Artificial Intelligence Project,
Memo AIM-110.
3. R.M. Burstall, (1970), "Formal Description of Program Structure
and Semantics in First Order Logic", in Machine Intelligence 5,
Edinburgh University Press, 79-98.
4. J. W. de Bakker, (1968), "Axiomatics of Simple Assignment
Statements", Publication of Mathematrsch Centrum, Amsterdam,
June 1968.
5. Donovan and Ledgard (1967), "A Formal System for the
Specification of the Syntax and Translation of Computer
Languages", Proc. FJCC 1967.
6. R.W. Floyd, (1967), "Assigning Meaning to Programs", Proceeding
of Symposia in Applied Mathematics, American Mathematical
Society, Vol. 19, 19-32.
7. P. Hayes, (1969), "A Machine-Oriented Formulation of the Extended
Functional Calculus", Memo AI-86, Artificial Intelligence
Project, Stanford University, April, 1969.
8. D. Knuth, (1968), "Semantics of Context-free Languages",
Mathematical System Theory, Vol. 2, No. 2.
9. H. Ledgard, (1969), "A Formal System for Defining the Syntax and
Semantics of Computer Languages", Ph.D. Thesis in Electrical
Engineering, M.I.T., April 1969.
10. P. Lucas, K. Alber, K. Bandat, H. Bekic, P. Oliva, K. Welk, G.
Zeisel, (1968), "Informal Introduction to the Abstract Syntax
and Interpretation of PL/1", Technical Report, IBM Laboratory,
Vienna, June 1968.
11. D.C. Luckham and D.M.R. Park, (1964), "The Undecidability of the
Equivalence Problem for Program Schemata", Report No. 1141,
Bolt, Beranek, and Newman, Cambridge, Massachusetts.
12. Z. Manna, (1968), "Termination of Algorithms", Ph.D.
Thesis, Computer Science Department, Carnegie-Mellon University.
13. Z. Manna, (1969a), "Properties of Programs and the First Order
Predicate Calculus", J. ACM, April 1969.
14. Z. Manna, (1969b), "The Correctness of Programs", J. System and
Computer Sciences, May 1969.
15. Z. Manna, (1970a), "The Correctness of Non-deterministic
Programs", Artificial Intelligence Journal, Vol. 1, No. 1.
16. Z. Manna, (1970b), "Second-order Mathematical Theory of
Computation", Proc. ACM Symposium on Theory of Computing (May,
1970).
17. Z. Manna and J. McCarthy, (1970), "Properties of Programs and
Partial Function Logic", in Machine Intelligence 5, Edinburgh
University Press.
18. Z. Manna and S. Ness, "On the Termination of Markov Algorithms",
Proceedings of the third Hawaii International Conference on
Systems Sciences, January 1970.
19. Z. Manna and A. Pneuli, (1969c), "Formalization of Properties of
Recursively Defined Functions", Proc. ACM Symposium on Computing
Theory, May 1969. To appear in the Journal.ACM (July 1970).
20. J. McCarthy (1963a), "A Basis for a Mathematical Theory of
Computation", in Braffort and Hirschberg (eds), Computer
Programming and Formal Systems, North-Holland, Amsterdam.
21. J. McCarthy, (1963b), "Towards a Mathematical Theory of
Computation", Proc. IFIP Congress 62, North-Holland, Amsterdam.
22. J. McCarthy, (1963c), "Predicate Calculus with 'Undefined' as a
Truth-Value", A.I. Memo, #1, Stanford Artificial Intelligence
Project, Stanford University, March 1963.
23. J. McCarthy, (1964), "A Proof-Checker for Predicate Calculus",
A.I. Memo #27, Stanford Artificial Intelligence Project,
Stanford University.
24. J. McCarthy, (1965), "Problems in the Theory of Computation",
Proc. IFIP Congress 65.
25. J. McCarthy, (1966), "A Formal Description of a Subset of
Algol", pp 1-12 of Formal Language Description Languages for
Computer Programming, T.B. Steel, Jr. (editor), North-Holland
Publishing Co., Amsterdam.
26. J. McCarthy and J. Painter, (1967), "Correctness of a Compiler
for Arithmetic Expressions", in Amer. Math. Soc. Proceedings
of Symposia in Applied Mathematics, Mathematical Aspects
Aspects of Computer Science, New York.
27. L. Morris, (1970), Forthcoming Ph.D. Thesis, Stanford
University.
28. J. Painter, (1967), "Semantic Correctness of a Compiler for an
Algol-like Language", Ph.D. Thesis in Computer Science, Stanford
University.
29. D. Park (1970),"Fixpoint Induction and Proofs of Program Proper-
ties", in Machine Intelligence 5, Edinburgh University Press.
30. Robinson, (1965), "A Machine-Oriented Logic Based on the
Resolution Principle", JACM, 12, 23-41.
31. D. Scott, (1970), unpublished memo.
32. J.D. Rutledge, (1964), "On Ianovs Program Schemata", JACM, Vol.
11, No. 1, January 1964.
33. H. Wang, (1961), "The Calculus of Partial Predicates and its
Extension to Set Theory", Zeitschr f. Math., Logik und
Grundladen a. Math., pp 283-288.
34. Y.I. Yanov, (1960), "The Logical Schemes of Algorithms",
Problems of Cybernetics, Vol. 1, translated from the Russian by
Nadler, Griffiths, Kiss, and Muir, Pergamon Press, New York.